Often it is difficult to verify whether software will perform the tasks that it was designed to perform. Accordingly, proofs are commonly written that specify what a piece of software is supposed to do and how to test that the software does what it is supposed to do.
Programs are constantly evolving. Even if verification is performed on one version of a program, that verification does not apply for any future versions of the program. Verification of programs should be performed each time a new version of code for the program is generated to ensure that the same safety guarantees for all subsequent releases of the program are maintained. For example, any formal proof about a program should be checked again with each new update to ensure that all safety properties certified by the proof are still guaranteed. However, verifying a particular version of a program (e.g., checking a proof) is a computationally expensive process and can take many hours to complete (e.g., up to 10 hours or longer). Moreover, verifying a version of a program by checking a proof for that program generally requires setting up a software stack that includes specialized verification tools (also referred to as proving technologies).